T:Type, l:(T List), x:T. no_repeats(T; cons(x; l))  (no_repeats(T; l)  ((x  l))) 

latex

Definitions	prop{i:l}, t  T, P  Q, Y, ||as||, P  Q, P  Q, no_repeats(T; l), P  Q, x:A. B(x), T, True, False, A  B, A, ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), guard(T), sq_type(T), l[i], A c B, x:A. B(x), (x  l), , P  Q, decidable(P)
Lemmas	l member wf, non neg length, length cons, select wf, length wf1, nat wf, not wf, select cons tl, le wf, true wf, squash wf, decidable int equal